0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 86 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 33 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 59 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 AND
↳9 PiDP
↳10 UsableRulesProof (⇔, 0 ms)
↳11 PiDP
↳12 PiDPToQDPProof (⇔, 2 ms)
↳13 QDP
↳14 QDPSizeChangeProof (⇔, 0 ms)
↳15 YES
↳16 PiDP
↳17 UsableRulesProof (⇔, 0 ms)
↳18 PiDP
↳19 PiDPToQDPProof (⇒, 0 ms)
↳20 QDP
↳21 QDPSizeChangeProof (⇔, 0 ms)
↳22 YES
↳23 PiDP
↳24 UsableRulesProof (⇔, 0 ms)
↳25 PiDP
↳26 PiDPToQDPProof (⇔, 0 ms)
↳27 QDP
↳28 QDPSizeChangeProof (⇔, 0 ms)
↳29 YES
perm1E_in_gg([], []) → perm1E_out_gg([], [])
perm1E_in_gg(.(T15, T16), .(T17, T18)) → U8_gg(T15, T16, T17, T18, eq_len1A_in_gg(T16, T18))
eq_len1A_in_gg([], []) → eq_len1A_out_gg([], [])
eq_len1A_in_gg(.(T27, T28), .(T29, T30)) → U1_gg(T27, T28, T29, T30, eq_len1A_in_gg(T28, T30))
U1_gg(T27, T28, T29, T30, eq_len1A_out_gg(T28, T30)) → eq_len1A_out_gg(.(T27, T28), .(T29, T30))
U8_gg(T15, T16, T17, T18, eq_len1A_out_gg(T16, T18)) → perm1E_out_gg(.(T15, T16), .(T17, T18))
perm1E_in_gg(.(T43, T44), .(T45, T46)) → U9_gg(T43, T44, T45, T46, eq_len1A_in_gg(T44, T46))
U9_gg(T43, T44, T45, T46, eq_len1A_out_gg(T44, T46)) → U10_gg(T43, T44, T45, T46, pC_in_gggg(T43, T45, T46, T44))
pC_in_gggg(T43, T45, T46, T44) → U3_gggg(T43, T45, T46, T44, memberD_in_ggg(T43, T45, T46))
memberD_in_ggg(T63, T63, T64) → memberD_out_ggg(T63, T63, T64)
memberD_in_ggg(T75, T76, T77) → U7_ggg(T75, T76, T77, memberB_in_gg(T75, T77))
memberB_in_gg(T90, .(T90, T91)) → memberB_out_gg(T90, .(T90, T91))
memberB_in_gg(T98, .(T99, T100)) → U2_gg(T98, T99, T100, memberB_in_gg(T98, T100))
U2_gg(T98, T99, T100, memberB_out_gg(T98, T100)) → memberB_out_gg(T98, .(T99, T100))
U7_ggg(T75, T76, T77, memberB_out_gg(T75, T77)) → memberD_out_ggg(T75, T76, T77)
U3_gggg(T43, T45, T46, T44, memberD_out_ggg(T43, T45, T46)) → pC_out_gggg(T43, T45, T46, T44)
pC_in_gggg(T43, T117, T118, []) → U4_gggg(T43, T117, T118, memberD_in_ggg(T43, T117, T118))
U4_gggg(T43, T117, T118, memberD_out_ggg(T43, T117, T118)) → pC_out_gggg(T43, T117, T118, [])
pC_in_gggg(T43, T129, T130, .(T127, T128)) → U5_gggg(T43, T129, T130, T127, T128, memberD_in_ggg(T43, T129, T130))
U5_gggg(T43, T129, T130, T127, T128, memberD_out_ggg(T43, T129, T130)) → U6_gggg(T43, T129, T130, T127, T128, pC_in_gggg(T127, T129, T130, T128))
U6_gggg(T43, T129, T130, T127, T128, pC_out_gggg(T127, T129, T130, T128)) → pC_out_gggg(T43, T129, T130, .(T127, T128))
U10_gg(T43, T44, T45, T46, pC_out_gggg(T43, T45, T46, T44)) → perm1E_out_gg(.(T43, T44), .(T45, T46))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
perm1E_in_gg([], []) → perm1E_out_gg([], [])
perm1E_in_gg(.(T15, T16), .(T17, T18)) → U8_gg(T15, T16, T17, T18, eq_len1A_in_gg(T16, T18))
eq_len1A_in_gg([], []) → eq_len1A_out_gg([], [])
eq_len1A_in_gg(.(T27, T28), .(T29, T30)) → U1_gg(T27, T28, T29, T30, eq_len1A_in_gg(T28, T30))
U1_gg(T27, T28, T29, T30, eq_len1A_out_gg(T28, T30)) → eq_len1A_out_gg(.(T27, T28), .(T29, T30))
U8_gg(T15, T16, T17, T18, eq_len1A_out_gg(T16, T18)) → perm1E_out_gg(.(T15, T16), .(T17, T18))
perm1E_in_gg(.(T43, T44), .(T45, T46)) → U9_gg(T43, T44, T45, T46, eq_len1A_in_gg(T44, T46))
U9_gg(T43, T44, T45, T46, eq_len1A_out_gg(T44, T46)) → U10_gg(T43, T44, T45, T46, pC_in_gggg(T43, T45, T46, T44))
pC_in_gggg(T43, T45, T46, T44) → U3_gggg(T43, T45, T46, T44, memberD_in_ggg(T43, T45, T46))
memberD_in_ggg(T63, T63, T64) → memberD_out_ggg(T63, T63, T64)
memberD_in_ggg(T75, T76, T77) → U7_ggg(T75, T76, T77, memberB_in_gg(T75, T77))
memberB_in_gg(T90, .(T90, T91)) → memberB_out_gg(T90, .(T90, T91))
memberB_in_gg(T98, .(T99, T100)) → U2_gg(T98, T99, T100, memberB_in_gg(T98, T100))
U2_gg(T98, T99, T100, memberB_out_gg(T98, T100)) → memberB_out_gg(T98, .(T99, T100))
U7_ggg(T75, T76, T77, memberB_out_gg(T75, T77)) → memberD_out_ggg(T75, T76, T77)
U3_gggg(T43, T45, T46, T44, memberD_out_ggg(T43, T45, T46)) → pC_out_gggg(T43, T45, T46, T44)
pC_in_gggg(T43, T117, T118, []) → U4_gggg(T43, T117, T118, memberD_in_ggg(T43, T117, T118))
U4_gggg(T43, T117, T118, memberD_out_ggg(T43, T117, T118)) → pC_out_gggg(T43, T117, T118, [])
pC_in_gggg(T43, T129, T130, .(T127, T128)) → U5_gggg(T43, T129, T130, T127, T128, memberD_in_ggg(T43, T129, T130))
U5_gggg(T43, T129, T130, T127, T128, memberD_out_ggg(T43, T129, T130)) → U6_gggg(T43, T129, T130, T127, T128, pC_in_gggg(T127, T129, T130, T128))
U6_gggg(T43, T129, T130, T127, T128, pC_out_gggg(T127, T129, T130, T128)) → pC_out_gggg(T43, T129, T130, .(T127, T128))
U10_gg(T43, T44, T45, T46, pC_out_gggg(T43, T45, T46, T44)) → perm1E_out_gg(.(T43, T44), .(T45, T46))
PERM1E_IN_GG(.(T15, T16), .(T17, T18)) → U8_GG(T15, T16, T17, T18, eq_len1A_in_gg(T16, T18))
PERM1E_IN_GG(.(T15, T16), .(T17, T18)) → EQ_LEN1A_IN_GG(T16, T18)
EQ_LEN1A_IN_GG(.(T27, T28), .(T29, T30)) → U1_GG(T27, T28, T29, T30, eq_len1A_in_gg(T28, T30))
EQ_LEN1A_IN_GG(.(T27, T28), .(T29, T30)) → EQ_LEN1A_IN_GG(T28, T30)
PERM1E_IN_GG(.(T43, T44), .(T45, T46)) → U9_GG(T43, T44, T45, T46, eq_len1A_in_gg(T44, T46))
U9_GG(T43, T44, T45, T46, eq_len1A_out_gg(T44, T46)) → U10_GG(T43, T44, T45, T46, pC_in_gggg(T43, T45, T46, T44))
U9_GG(T43, T44, T45, T46, eq_len1A_out_gg(T44, T46)) → PC_IN_GGGG(T43, T45, T46, T44)
PC_IN_GGGG(T43, T45, T46, T44) → U3_GGGG(T43, T45, T46, T44, memberD_in_ggg(T43, T45, T46))
PC_IN_GGGG(T43, T45, T46, T44) → MEMBERD_IN_GGG(T43, T45, T46)
MEMBERD_IN_GGG(T75, T76, T77) → U7_GGG(T75, T76, T77, memberB_in_gg(T75, T77))
MEMBERD_IN_GGG(T75, T76, T77) → MEMBERB_IN_GG(T75, T77)
MEMBERB_IN_GG(T98, .(T99, T100)) → U2_GG(T98, T99, T100, memberB_in_gg(T98, T100))
MEMBERB_IN_GG(T98, .(T99, T100)) → MEMBERB_IN_GG(T98, T100)
PC_IN_GGGG(T43, T117, T118, []) → U4_GGGG(T43, T117, T118, memberD_in_ggg(T43, T117, T118))
PC_IN_GGGG(T43, T117, T118, []) → MEMBERD_IN_GGG(T43, T117, T118)
PC_IN_GGGG(T43, T129, T130, .(T127, T128)) → U5_GGGG(T43, T129, T130, T127, T128, memberD_in_ggg(T43, T129, T130))
PC_IN_GGGG(T43, T129, T130, .(T127, T128)) → MEMBERD_IN_GGG(T43, T129, T130)
U5_GGGG(T43, T129, T130, T127, T128, memberD_out_ggg(T43, T129, T130)) → U6_GGGG(T43, T129, T130, T127, T128, pC_in_gggg(T127, T129, T130, T128))
U5_GGGG(T43, T129, T130, T127, T128, memberD_out_ggg(T43, T129, T130)) → PC_IN_GGGG(T127, T129, T130, T128)
perm1E_in_gg([], []) → perm1E_out_gg([], [])
perm1E_in_gg(.(T15, T16), .(T17, T18)) → U8_gg(T15, T16, T17, T18, eq_len1A_in_gg(T16, T18))
eq_len1A_in_gg([], []) → eq_len1A_out_gg([], [])
eq_len1A_in_gg(.(T27, T28), .(T29, T30)) → U1_gg(T27, T28, T29, T30, eq_len1A_in_gg(T28, T30))
U1_gg(T27, T28, T29, T30, eq_len1A_out_gg(T28, T30)) → eq_len1A_out_gg(.(T27, T28), .(T29, T30))
U8_gg(T15, T16, T17, T18, eq_len1A_out_gg(T16, T18)) → perm1E_out_gg(.(T15, T16), .(T17, T18))
perm1E_in_gg(.(T43, T44), .(T45, T46)) → U9_gg(T43, T44, T45, T46, eq_len1A_in_gg(T44, T46))
U9_gg(T43, T44, T45, T46, eq_len1A_out_gg(T44, T46)) → U10_gg(T43, T44, T45, T46, pC_in_gggg(T43, T45, T46, T44))
pC_in_gggg(T43, T45, T46, T44) → U3_gggg(T43, T45, T46, T44, memberD_in_ggg(T43, T45, T46))
memberD_in_ggg(T63, T63, T64) → memberD_out_ggg(T63, T63, T64)
memberD_in_ggg(T75, T76, T77) → U7_ggg(T75, T76, T77, memberB_in_gg(T75, T77))
memberB_in_gg(T90, .(T90, T91)) → memberB_out_gg(T90, .(T90, T91))
memberB_in_gg(T98, .(T99, T100)) → U2_gg(T98, T99, T100, memberB_in_gg(T98, T100))
U2_gg(T98, T99, T100, memberB_out_gg(T98, T100)) → memberB_out_gg(T98, .(T99, T100))
U7_ggg(T75, T76, T77, memberB_out_gg(T75, T77)) → memberD_out_ggg(T75, T76, T77)
U3_gggg(T43, T45, T46, T44, memberD_out_ggg(T43, T45, T46)) → pC_out_gggg(T43, T45, T46, T44)
pC_in_gggg(T43, T117, T118, []) → U4_gggg(T43, T117, T118, memberD_in_ggg(T43, T117, T118))
U4_gggg(T43, T117, T118, memberD_out_ggg(T43, T117, T118)) → pC_out_gggg(T43, T117, T118, [])
pC_in_gggg(T43, T129, T130, .(T127, T128)) → U5_gggg(T43, T129, T130, T127, T128, memberD_in_ggg(T43, T129, T130))
U5_gggg(T43, T129, T130, T127, T128, memberD_out_ggg(T43, T129, T130)) → U6_gggg(T43, T129, T130, T127, T128, pC_in_gggg(T127, T129, T130, T128))
U6_gggg(T43, T129, T130, T127, T128, pC_out_gggg(T127, T129, T130, T128)) → pC_out_gggg(T43, T129, T130, .(T127, T128))
U10_gg(T43, T44, T45, T46, pC_out_gggg(T43, T45, T46, T44)) → perm1E_out_gg(.(T43, T44), .(T45, T46))
PERM1E_IN_GG(.(T15, T16), .(T17, T18)) → U8_GG(T15, T16, T17, T18, eq_len1A_in_gg(T16, T18))
PERM1E_IN_GG(.(T15, T16), .(T17, T18)) → EQ_LEN1A_IN_GG(T16, T18)
EQ_LEN1A_IN_GG(.(T27, T28), .(T29, T30)) → U1_GG(T27, T28, T29, T30, eq_len1A_in_gg(T28, T30))
EQ_LEN1A_IN_GG(.(T27, T28), .(T29, T30)) → EQ_LEN1A_IN_GG(T28, T30)
PERM1E_IN_GG(.(T43, T44), .(T45, T46)) → U9_GG(T43, T44, T45, T46, eq_len1A_in_gg(T44, T46))
U9_GG(T43, T44, T45, T46, eq_len1A_out_gg(T44, T46)) → U10_GG(T43, T44, T45, T46, pC_in_gggg(T43, T45, T46, T44))
U9_GG(T43, T44, T45, T46, eq_len1A_out_gg(T44, T46)) → PC_IN_GGGG(T43, T45, T46, T44)
PC_IN_GGGG(T43, T45, T46, T44) → U3_GGGG(T43, T45, T46, T44, memberD_in_ggg(T43, T45, T46))
PC_IN_GGGG(T43, T45, T46, T44) → MEMBERD_IN_GGG(T43, T45, T46)
MEMBERD_IN_GGG(T75, T76, T77) → U7_GGG(T75, T76, T77, memberB_in_gg(T75, T77))
MEMBERD_IN_GGG(T75, T76, T77) → MEMBERB_IN_GG(T75, T77)
MEMBERB_IN_GG(T98, .(T99, T100)) → U2_GG(T98, T99, T100, memberB_in_gg(T98, T100))
MEMBERB_IN_GG(T98, .(T99, T100)) → MEMBERB_IN_GG(T98, T100)
PC_IN_GGGG(T43, T117, T118, []) → U4_GGGG(T43, T117, T118, memberD_in_ggg(T43, T117, T118))
PC_IN_GGGG(T43, T117, T118, []) → MEMBERD_IN_GGG(T43, T117, T118)
PC_IN_GGGG(T43, T129, T130, .(T127, T128)) → U5_GGGG(T43, T129, T130, T127, T128, memberD_in_ggg(T43, T129, T130))
PC_IN_GGGG(T43, T129, T130, .(T127, T128)) → MEMBERD_IN_GGG(T43, T129, T130)
U5_GGGG(T43, T129, T130, T127, T128, memberD_out_ggg(T43, T129, T130)) → U6_GGGG(T43, T129, T130, T127, T128, pC_in_gggg(T127, T129, T130, T128))
U5_GGGG(T43, T129, T130, T127, T128, memberD_out_ggg(T43, T129, T130)) → PC_IN_GGGG(T127, T129, T130, T128)
perm1E_in_gg([], []) → perm1E_out_gg([], [])
perm1E_in_gg(.(T15, T16), .(T17, T18)) → U8_gg(T15, T16, T17, T18, eq_len1A_in_gg(T16, T18))
eq_len1A_in_gg([], []) → eq_len1A_out_gg([], [])
eq_len1A_in_gg(.(T27, T28), .(T29, T30)) → U1_gg(T27, T28, T29, T30, eq_len1A_in_gg(T28, T30))
U1_gg(T27, T28, T29, T30, eq_len1A_out_gg(T28, T30)) → eq_len1A_out_gg(.(T27, T28), .(T29, T30))
U8_gg(T15, T16, T17, T18, eq_len1A_out_gg(T16, T18)) → perm1E_out_gg(.(T15, T16), .(T17, T18))
perm1E_in_gg(.(T43, T44), .(T45, T46)) → U9_gg(T43, T44, T45, T46, eq_len1A_in_gg(T44, T46))
U9_gg(T43, T44, T45, T46, eq_len1A_out_gg(T44, T46)) → U10_gg(T43, T44, T45, T46, pC_in_gggg(T43, T45, T46, T44))
pC_in_gggg(T43, T45, T46, T44) → U3_gggg(T43, T45, T46, T44, memberD_in_ggg(T43, T45, T46))
memberD_in_ggg(T63, T63, T64) → memberD_out_ggg(T63, T63, T64)
memberD_in_ggg(T75, T76, T77) → U7_ggg(T75, T76, T77, memberB_in_gg(T75, T77))
memberB_in_gg(T90, .(T90, T91)) → memberB_out_gg(T90, .(T90, T91))
memberB_in_gg(T98, .(T99, T100)) → U2_gg(T98, T99, T100, memberB_in_gg(T98, T100))
U2_gg(T98, T99, T100, memberB_out_gg(T98, T100)) → memberB_out_gg(T98, .(T99, T100))
U7_ggg(T75, T76, T77, memberB_out_gg(T75, T77)) → memberD_out_ggg(T75, T76, T77)
U3_gggg(T43, T45, T46, T44, memberD_out_ggg(T43, T45, T46)) → pC_out_gggg(T43, T45, T46, T44)
pC_in_gggg(T43, T117, T118, []) → U4_gggg(T43, T117, T118, memberD_in_ggg(T43, T117, T118))
U4_gggg(T43, T117, T118, memberD_out_ggg(T43, T117, T118)) → pC_out_gggg(T43, T117, T118, [])
pC_in_gggg(T43, T129, T130, .(T127, T128)) → U5_gggg(T43, T129, T130, T127, T128, memberD_in_ggg(T43, T129, T130))
U5_gggg(T43, T129, T130, T127, T128, memberD_out_ggg(T43, T129, T130)) → U6_gggg(T43, T129, T130, T127, T128, pC_in_gggg(T127, T129, T130, T128))
U6_gggg(T43, T129, T130, T127, T128, pC_out_gggg(T127, T129, T130, T128)) → pC_out_gggg(T43, T129, T130, .(T127, T128))
U10_gg(T43, T44, T45, T46, pC_out_gggg(T43, T45, T46, T44)) → perm1E_out_gg(.(T43, T44), .(T45, T46))
MEMBERB_IN_GG(T98, .(T99, T100)) → MEMBERB_IN_GG(T98, T100)
perm1E_in_gg([], []) → perm1E_out_gg([], [])
perm1E_in_gg(.(T15, T16), .(T17, T18)) → U8_gg(T15, T16, T17, T18, eq_len1A_in_gg(T16, T18))
eq_len1A_in_gg([], []) → eq_len1A_out_gg([], [])
eq_len1A_in_gg(.(T27, T28), .(T29, T30)) → U1_gg(T27, T28, T29, T30, eq_len1A_in_gg(T28, T30))
U1_gg(T27, T28, T29, T30, eq_len1A_out_gg(T28, T30)) → eq_len1A_out_gg(.(T27, T28), .(T29, T30))
U8_gg(T15, T16, T17, T18, eq_len1A_out_gg(T16, T18)) → perm1E_out_gg(.(T15, T16), .(T17, T18))
perm1E_in_gg(.(T43, T44), .(T45, T46)) → U9_gg(T43, T44, T45, T46, eq_len1A_in_gg(T44, T46))
U9_gg(T43, T44, T45, T46, eq_len1A_out_gg(T44, T46)) → U10_gg(T43, T44, T45, T46, pC_in_gggg(T43, T45, T46, T44))
pC_in_gggg(T43, T45, T46, T44) → U3_gggg(T43, T45, T46, T44, memberD_in_ggg(T43, T45, T46))
memberD_in_ggg(T63, T63, T64) → memberD_out_ggg(T63, T63, T64)
memberD_in_ggg(T75, T76, T77) → U7_ggg(T75, T76, T77, memberB_in_gg(T75, T77))
memberB_in_gg(T90, .(T90, T91)) → memberB_out_gg(T90, .(T90, T91))
memberB_in_gg(T98, .(T99, T100)) → U2_gg(T98, T99, T100, memberB_in_gg(T98, T100))
U2_gg(T98, T99, T100, memberB_out_gg(T98, T100)) → memberB_out_gg(T98, .(T99, T100))
U7_ggg(T75, T76, T77, memberB_out_gg(T75, T77)) → memberD_out_ggg(T75, T76, T77)
U3_gggg(T43, T45, T46, T44, memberD_out_ggg(T43, T45, T46)) → pC_out_gggg(T43, T45, T46, T44)
pC_in_gggg(T43, T117, T118, []) → U4_gggg(T43, T117, T118, memberD_in_ggg(T43, T117, T118))
U4_gggg(T43, T117, T118, memberD_out_ggg(T43, T117, T118)) → pC_out_gggg(T43, T117, T118, [])
pC_in_gggg(T43, T129, T130, .(T127, T128)) → U5_gggg(T43, T129, T130, T127, T128, memberD_in_ggg(T43, T129, T130))
U5_gggg(T43, T129, T130, T127, T128, memberD_out_ggg(T43, T129, T130)) → U6_gggg(T43, T129, T130, T127, T128, pC_in_gggg(T127, T129, T130, T128))
U6_gggg(T43, T129, T130, T127, T128, pC_out_gggg(T127, T129, T130, T128)) → pC_out_gggg(T43, T129, T130, .(T127, T128))
U10_gg(T43, T44, T45, T46, pC_out_gggg(T43, T45, T46, T44)) → perm1E_out_gg(.(T43, T44), .(T45, T46))
MEMBERB_IN_GG(T98, .(T99, T100)) → MEMBERB_IN_GG(T98, T100)
MEMBERB_IN_GG(T98, .(T99, T100)) → MEMBERB_IN_GG(T98, T100)
From the DPs we obtained the following set of size-change graphs:
PC_IN_GGGG(T43, T129, T130, .(T127, T128)) → U5_GGGG(T43, T129, T130, T127, T128, memberD_in_ggg(T43, T129, T130))
U5_GGGG(T43, T129, T130, T127, T128, memberD_out_ggg(T43, T129, T130)) → PC_IN_GGGG(T127, T129, T130, T128)
perm1E_in_gg([], []) → perm1E_out_gg([], [])
perm1E_in_gg(.(T15, T16), .(T17, T18)) → U8_gg(T15, T16, T17, T18, eq_len1A_in_gg(T16, T18))
eq_len1A_in_gg([], []) → eq_len1A_out_gg([], [])
eq_len1A_in_gg(.(T27, T28), .(T29, T30)) → U1_gg(T27, T28, T29, T30, eq_len1A_in_gg(T28, T30))
U1_gg(T27, T28, T29, T30, eq_len1A_out_gg(T28, T30)) → eq_len1A_out_gg(.(T27, T28), .(T29, T30))
U8_gg(T15, T16, T17, T18, eq_len1A_out_gg(T16, T18)) → perm1E_out_gg(.(T15, T16), .(T17, T18))
perm1E_in_gg(.(T43, T44), .(T45, T46)) → U9_gg(T43, T44, T45, T46, eq_len1A_in_gg(T44, T46))
U9_gg(T43, T44, T45, T46, eq_len1A_out_gg(T44, T46)) → U10_gg(T43, T44, T45, T46, pC_in_gggg(T43, T45, T46, T44))
pC_in_gggg(T43, T45, T46, T44) → U3_gggg(T43, T45, T46, T44, memberD_in_ggg(T43, T45, T46))
memberD_in_ggg(T63, T63, T64) → memberD_out_ggg(T63, T63, T64)
memberD_in_ggg(T75, T76, T77) → U7_ggg(T75, T76, T77, memberB_in_gg(T75, T77))
memberB_in_gg(T90, .(T90, T91)) → memberB_out_gg(T90, .(T90, T91))
memberB_in_gg(T98, .(T99, T100)) → U2_gg(T98, T99, T100, memberB_in_gg(T98, T100))
U2_gg(T98, T99, T100, memberB_out_gg(T98, T100)) → memberB_out_gg(T98, .(T99, T100))
U7_ggg(T75, T76, T77, memberB_out_gg(T75, T77)) → memberD_out_ggg(T75, T76, T77)
U3_gggg(T43, T45, T46, T44, memberD_out_ggg(T43, T45, T46)) → pC_out_gggg(T43, T45, T46, T44)
pC_in_gggg(T43, T117, T118, []) → U4_gggg(T43, T117, T118, memberD_in_ggg(T43, T117, T118))
U4_gggg(T43, T117, T118, memberD_out_ggg(T43, T117, T118)) → pC_out_gggg(T43, T117, T118, [])
pC_in_gggg(T43, T129, T130, .(T127, T128)) → U5_gggg(T43, T129, T130, T127, T128, memberD_in_ggg(T43, T129, T130))
U5_gggg(T43, T129, T130, T127, T128, memberD_out_ggg(T43, T129, T130)) → U6_gggg(T43, T129, T130, T127, T128, pC_in_gggg(T127, T129, T130, T128))
U6_gggg(T43, T129, T130, T127, T128, pC_out_gggg(T127, T129, T130, T128)) → pC_out_gggg(T43, T129, T130, .(T127, T128))
U10_gg(T43, T44, T45, T46, pC_out_gggg(T43, T45, T46, T44)) → perm1E_out_gg(.(T43, T44), .(T45, T46))
PC_IN_GGGG(T43, T129, T130, .(T127, T128)) → U5_GGGG(T43, T129, T130, T127, T128, memberD_in_ggg(T43, T129, T130))
U5_GGGG(T43, T129, T130, T127, T128, memberD_out_ggg(T43, T129, T130)) → PC_IN_GGGG(T127, T129, T130, T128)
memberD_in_ggg(T63, T63, T64) → memberD_out_ggg(T63, T63, T64)
memberD_in_ggg(T75, T76, T77) → U7_ggg(T75, T76, T77, memberB_in_gg(T75, T77))
U7_ggg(T75, T76, T77, memberB_out_gg(T75, T77)) → memberD_out_ggg(T75, T76, T77)
memberB_in_gg(T90, .(T90, T91)) → memberB_out_gg(T90, .(T90, T91))
memberB_in_gg(T98, .(T99, T100)) → U2_gg(T98, T99, T100, memberB_in_gg(T98, T100))
U2_gg(T98, T99, T100, memberB_out_gg(T98, T100)) → memberB_out_gg(T98, .(T99, T100))
PC_IN_GGGG(T43, T129, T130, .(T127, T128)) → U5_GGGG(T129, T130, T127, T128, memberD_in_ggg(T43, T129, T130))
U5_GGGG(T129, T130, T127, T128, memberD_out_ggg) → PC_IN_GGGG(T127, T129, T130, T128)
memberD_in_ggg(T63, T63, T64) → memberD_out_ggg
memberD_in_ggg(T75, T76, T77) → U7_ggg(memberB_in_gg(T75, T77))
U7_ggg(memberB_out_gg) → memberD_out_ggg
memberB_in_gg(T90, .(T90, T91)) → memberB_out_gg
memberB_in_gg(T98, .(T99, T100)) → U2_gg(memberB_in_gg(T98, T100))
U2_gg(memberB_out_gg) → memberB_out_gg
memberD_in_ggg(x0, x1, x2)
U7_ggg(x0)
memberB_in_gg(x0, x1)
U2_gg(x0)
From the DPs we obtained the following set of size-change graphs:
EQ_LEN1A_IN_GG(.(T27, T28), .(T29, T30)) → EQ_LEN1A_IN_GG(T28, T30)
perm1E_in_gg([], []) → perm1E_out_gg([], [])
perm1E_in_gg(.(T15, T16), .(T17, T18)) → U8_gg(T15, T16, T17, T18, eq_len1A_in_gg(T16, T18))
eq_len1A_in_gg([], []) → eq_len1A_out_gg([], [])
eq_len1A_in_gg(.(T27, T28), .(T29, T30)) → U1_gg(T27, T28, T29, T30, eq_len1A_in_gg(T28, T30))
U1_gg(T27, T28, T29, T30, eq_len1A_out_gg(T28, T30)) → eq_len1A_out_gg(.(T27, T28), .(T29, T30))
U8_gg(T15, T16, T17, T18, eq_len1A_out_gg(T16, T18)) → perm1E_out_gg(.(T15, T16), .(T17, T18))
perm1E_in_gg(.(T43, T44), .(T45, T46)) → U9_gg(T43, T44, T45, T46, eq_len1A_in_gg(T44, T46))
U9_gg(T43, T44, T45, T46, eq_len1A_out_gg(T44, T46)) → U10_gg(T43, T44, T45, T46, pC_in_gggg(T43, T45, T46, T44))
pC_in_gggg(T43, T45, T46, T44) → U3_gggg(T43, T45, T46, T44, memberD_in_ggg(T43, T45, T46))
memberD_in_ggg(T63, T63, T64) → memberD_out_ggg(T63, T63, T64)
memberD_in_ggg(T75, T76, T77) → U7_ggg(T75, T76, T77, memberB_in_gg(T75, T77))
memberB_in_gg(T90, .(T90, T91)) → memberB_out_gg(T90, .(T90, T91))
memberB_in_gg(T98, .(T99, T100)) → U2_gg(T98, T99, T100, memberB_in_gg(T98, T100))
U2_gg(T98, T99, T100, memberB_out_gg(T98, T100)) → memberB_out_gg(T98, .(T99, T100))
U7_ggg(T75, T76, T77, memberB_out_gg(T75, T77)) → memberD_out_ggg(T75, T76, T77)
U3_gggg(T43, T45, T46, T44, memberD_out_ggg(T43, T45, T46)) → pC_out_gggg(T43, T45, T46, T44)
pC_in_gggg(T43, T117, T118, []) → U4_gggg(T43, T117, T118, memberD_in_ggg(T43, T117, T118))
U4_gggg(T43, T117, T118, memberD_out_ggg(T43, T117, T118)) → pC_out_gggg(T43, T117, T118, [])
pC_in_gggg(T43, T129, T130, .(T127, T128)) → U5_gggg(T43, T129, T130, T127, T128, memberD_in_ggg(T43, T129, T130))
U5_gggg(T43, T129, T130, T127, T128, memberD_out_ggg(T43, T129, T130)) → U6_gggg(T43, T129, T130, T127, T128, pC_in_gggg(T127, T129, T130, T128))
U6_gggg(T43, T129, T130, T127, T128, pC_out_gggg(T127, T129, T130, T128)) → pC_out_gggg(T43, T129, T130, .(T127, T128))
U10_gg(T43, T44, T45, T46, pC_out_gggg(T43, T45, T46, T44)) → perm1E_out_gg(.(T43, T44), .(T45, T46))
EQ_LEN1A_IN_GG(.(T27, T28), .(T29, T30)) → EQ_LEN1A_IN_GG(T28, T30)
EQ_LEN1A_IN_GG(.(T27, T28), .(T29, T30)) → EQ_LEN1A_IN_GG(T28, T30)
From the DPs we obtained the following set of size-change graphs: